| Definitions |  b, P   Q,  x:A. B(x), w-info(w;e), t  T, E,  x.A(x), kind(e), isrcv(k), islocal(k), x:A  B(x), w.M, Msg(M), (x l),  , w.TA, f(a), s = t, x:A  B(x), A c B,  x:A. B(x), P & Q, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), FairFifo, World, w-machine-constraint(w), loc(e), False, {x:A| B(x)} , IdLnk, Id, A  B,  , w.T, vartype(i;x), s(i;t).x, Type, kindcase(k; a.f(a); l,t.g(l;t) ), valtype(i;a), val(a), Knd, Void, S  T, outl(x), t.2, t.1, outr(x),  , isl(x),  ,   b, if b then t else f fi , Unit, left + right, type List, w-automaton(T;TA;M), <a, b>, w-machine(w;i),  , tag(k), lnk(k), act(k), suptype(S; T), let x,y,z = a in t(x;y;z), time(e), loc(e), a(i;t), isnull(a), A, kind(a), True, {T}, SQType(T), act(e), V(i;k), kind(e), val(e), P  Q,  T, P Q, s ~ t, sender(e), rcv?(e), #$n,  x,y. t(x;y), x. t(x), r + s, n+m, a < b, mlnk(m), source(l), m(i;t), msg(l;t;v), ecase1(e;info;i.f(i);l,e'.g(l;e')) |
| Lemmas | w-rcv-msg, w-time wf, l member wf, squash wf, w-loc wf, msg wf, lnk wf, tagof wf, pi1 wf, pi2 wf, nat wf, not wf, w-isnull wf, unit wf, Msg wf, w-m wf, lsrc wf, mlnk wf, le wf, w-vartype wf, qadd wf, kindcase wf, IdLnk wf, int inc rationals, rcv?-kind, sender wf, false wf, true wf, read-w-state-when, w-eval wf, w-kind-lemma, Id sq, isl wf, w-valtype wf, outl wf, actof wf, w-s wf, w-a wf, w-val wf, w-automaton wf, w-machine wf, ifthenelse wf, bnot wf, w-TA wf, Id wf, w-M wf, rationals wf, w-T wf, loc wf, w-kind wf, Knd wf, subtype rel self, w-loc-lemma, fair-fifo wf, world wf, w-E wf, islocal wf, assert wf, isrcv wf, kind wf, w-info wf |
